FDL - Step of Proof: or_true

Step of Proof: or_true_r

9,38

Inference at *
Iof proof for Lemma or true r:

. (A

True)

True

by ((((RepD)

CollapseTHENM (ProveProp1))

)

CollapseTHENA ((Auto_aux (first_nat 1:n

C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

Definitions t T, P Q, P Q, P Q, True, P Q, P Q, , x:A. B(x)

Lemmas true wf

Definitions	t T, P Q, P Q, P Q, True, P Q, P Q, , x:A. B(x)
Lemmas	true wf